package proof;

import atom.Atom;
import atom.UnaryAtom;
import formula.*;
import literal.UnaryLiteral;
import sign.FormulaSign;

import java.util.ArrayList;

public enum ProofRule {
    D1{
        public Formula applyRule(ArrayList<Proof> f){//{ANY(q,l),Exist(p,q)}D1 -> Exist(p,l)
            // f.size() != 2 return null
            if (f.size()!=2){return null;}
            // f[0] not BinaryFormula return null
            if (f.get(0).getConclusion() instanceof BinaryFormula){}else {
                return null;
            }
            BinaryFormula f1=(BinaryFormula) f.get(0).getConclusion();
            if (f.get(1).getConclusion() instanceof BinaryFormula){}else {
                return null;
            }
            BinaryFormula f2=(BinaryFormula) f.get(1).getConclusion();

            boolean flag1=f1.getLeft() instanceof UnaryFormula;
            boolean flag2=f2.getLeft() instanceof UnaryFormula;
            boolean flag3=f2.getRight() instanceof UnaryFormula;
            boolean flag=flag1 && flag2 && flag3;
            if (flag){//此时只有f1.getRight可不为uf（即可为bf或者uf）
                if (f1.getSign()==FormulaSign.ANY && f2.getSign()==FormulaSign.EXIST){
                    if (f1.getLeft().equals(f2.getRight())){
                        return new BinaryFormula(FormulaSign.EXIST,f2.getLeft(),f1.getRight());
                    }
                }
            }else {return null;}

            return null;
        }

            public String getRuleName(){
            return "D1";
        }
    },

    D2{//
        public Formula applyRule(ArrayList<Proof> f){
            // f.size() != 2 return null
            if (f.size()!=2){return null;}
            // f[0] not BinaryFormula return null
            if (f.get(0).getConclusion() instanceof BinaryFormula){}else {
                return null;
            }
            BinaryFormula f1=(BinaryFormula) f.get(0).getConclusion();
            if (f.get(1).getConclusion() instanceof BinaryFormula){}else {
                return null;
            }
            BinaryFormula f2=(BinaryFormula) f.get(1).getConclusion();

            boolean flag1=f1.getLeft() instanceof UnaryFormula;
            boolean flag2=f1.getRight() instanceof UnaryFormula;
            boolean flag3=f2.getLeft() instanceof UnaryFormula;
            boolean flag=flag1 && flag2 && flag3;
            if (flag){//此时只有f2.getRight可不为uf（即可为bf或者uf）
                if (f1.getSign()==FormulaSign.ANY && f2.getSign()==FormulaSign.EXIST){
                    if (f1.getLeft().equals(f2.getLeft())){
                        return new BinaryFormula(FormulaSign.EXIST,f1.getRight(),f2.getRight());
                    }
                }
            }else {return null;}
            return null;
        }
        public String getRuleName(){
            return "D2";
        }
        },
    D3{//D3的两种情况，要么两个formula都是BF,要么两个都是TF
        public Formula applyRule(ArrayList<Proof> f){
            // f.size() != 2 return null
            if (f.size()!=2){return null;}
            //BF情况
            // f[0] not BinaryFormula return null
            // f[1] not BinaryFormula return null
            if (f.get(0).getConclusion() instanceof BinaryFormula && f.get(1).getConclusion() instanceof BinaryFormula){
                BinaryFormula f1=(BinaryFormula) f.get(0).getConclusion();
                BinaryFormula f2=(BinaryFormula) f.get(1).getConclusion();

                boolean flag1=f1.getLeft() instanceof UnaryFormula;
                boolean flag2=f2.getLeft() instanceof UnaryFormula;
                if (flag1 && flag2){ }else { return null; }

                if (f1.getSign()==FormulaSign.ANY && f2.getSign()==FormulaSign.EXIST){
                    Formula f1_right= f1.getRight();//此处用Formula，可以为uf，也可以是bf
                    Formula f2_right= f2.getRight();
                    boolean flag = f1_right.isNegated(f2_right);//若互斥，则返回true，D3可以被apply
                    if (flag){
                        Formula f1_left= f1.getLeft();
                        return new BinaryFormula(FormulaSign.EXIST,f2.getLeft(),f1_left.getNegated());
                    }
                }
            }else {
                return null;
            }
            return null;
        }
        public String getRuleName(){
            return "D3";
        }
    },

      //返回值实现有问题
    A{
        public Formula applyRule(ArrayList<Proof> f){//ANY(p,not_p)A-> ANY(p,l)
            //注意：A rule只有一个输入
            // f.size() != 1 return null
            if (f.size()!=1){return null;}
            // f[0] not BinaryFormula return null
            if (f.get(0).getConclusion() instanceof BinaryFormula){}else {
                return null;
            }
            BinaryFormula f1=(BinaryFormula) f.get(0).getConclusion();

            boolean flag1=f1.getLeft() instanceof UnaryFormula;
            boolean flag2=f1.getRight() instanceof UnaryFormula;
            if (flag1 && flag2){}else {return null;}//f1的left和right都必须为uf

            Formula fl=f1.getLeft();
            Formula fr=f1.getRight();
            StarFormula star=new StarFormula();
            if (fl.isNegated(fr)){//存在uf，bf情况（现在应该只有uf情况）
                BinaryFormula result=new BinaryFormula(FormulaSign.ANY,fl,star);
                return result;
            }
          return null;
        }
        public String getRuleName(){
            return "A";
        }
    },

    B{
        public Formula applyRule(ArrayList<Proof> f){//{ANY(p,q),ANY(q,l)}B -> ANY(p,l)
            // f.size() != 2 return null
            if (f.size()!=2){return null;}
            //BF情况,两个都是BF
            // f[0] not BinaryFormula return null
            // f[1] not BinaryFormula return null
            if (f.get(0).getConclusion() instanceof BinaryFormula && f.get(1).getConclusion() instanceof BinaryFormula){
                BinaryFormula f1=(BinaryFormula) f.get(0).getConclusion();
                BinaryFormula f2=(BinaryFormula) f.get(1).getConclusion();

                boolean flag1=f1.getLeft() instanceof UnaryFormula;
                boolean flag2=f1.getRight() instanceof UnaryFormula;
                boolean flag3=f2.getLeft() instanceof UnaryFormula;
                boolean flag=flag1 && flag2 && flag3;

                if (flag){}else {return null;}//只有f2的right可同时为uf或者bf

                if (f1.getSign()==FormulaSign.ANY && f2.getSign()==FormulaSign.ANY){
                    if (f1.getRight().equals(f2.getLeft())){
                        return new BinaryFormula(FormulaSign.ANY,f1.getLeft(),f2.getRight());
                    }
                }
            }
            else {
                return null;
            }
            return null;
        }
        public String getRuleName(){
            return "B";
        }
    },

    I{
        public Formula applyRule(ArrayList<Proof> f){//{EXIST(p,l)}I -> EXIST(p,p)
            // f.size() != 1 return null
            if (f.size()!=1){return null;}
            if (f.get(0).getConclusion() instanceof BinaryFormula){
                BinaryFormula f1=(BinaryFormula) f.get(0).getConclusion();

                if (f1.getLeft() instanceof UnaryFormula){}else {return null;}//f1.left必须为uf

                if (f1.getSign()==FormulaSign.EXIST){
                    Formula atom=f1.getLeft();
                    BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,atom,atom);
                    return bf;
                }
            }
            return null;
        }
        public String getRuleName(){
            return "I";
        }
    },

    AA{//
        public Formula applyRule(ArrayList<Proof> f){
            // f.size() != 2 return null
            if (f.size()!=2){return null;}
            // f[0] not TripleFormula(现在是BF了) return null
            if (f.get(0).getConclusion() instanceof BinaryFormula){}else {
                return null;
            }
            // f[1] not BinaryFormula return null
            if (f.get(1).getConclusion() instanceof BinaryFormula){}else {
                return null;
            }
            //f[0]为tripleFormula
            BinaryFormula tf=(BinaryFormula) f.get(0).getConclusion();
            //if (tf.getLeft() instanceof UnaryFormula){}else {return null;}//tf.lef必须为uf(第225行做了相同的事情，这行可以被注释)
            //判定f[1]中的两个formula是不是related的
            BinaryFormula bf=(BinaryFormula) f.get(1).getConclusion();

            if (bf.getLeft() instanceof BinaryFormula || bf.getRight() instanceof BinaryFormula){//此时bf中应该是两个uf：q和q‘
                return null;
            }else {
                UnaryFormula bf_left=(UnaryFormula) bf.getLeft();//这里可以转换成uf类型，因为强制限定了q和q’是uf
                UnaryFormula bf_right=(UnaryFormula) bf.getRight();
                //例子中的情况都是（q，qR）不确定存不存在（qR，q）的情况。目前只进行（q，qR）的情况判断，日后有需要再添加
                if (bf.getSign()==FormulaSign.EXIST){
                    //条件满足，开始hasRelation的判断
                    if (bf_left.hasRelationWith(bf_right)){//binaryFormula方面所有条件满足，开始进行TripleFormula的条件判断
                        if (tf.getSign()==FormulaSign.ANY && tf.getRight() instanceof BinaryFormula){
                            if(tf.getLeft() instanceof BinaryFormula || tf.getRight() instanceof UnaryFormula){//新增，确保tf的left必定为uf,right必为bf
                                return null;
                            }
                            //System.out.println(tf);
                            UnaryFormula tf_left=(UnaryFormula) tf.getLeft();
                            BinaryFormula tf_right=(BinaryFormula) tf.getRight();
                            if (tf_right.getLeft() instanceof UnaryFormula){}else {return null;}//确保tf.right.left(此处为q)，必须是uf
                            if (tf_right.getSign()==FormulaSign.ANY){
                                UnaryFormula inner_related=(UnaryFormula) tf_right.getLeft();
                                if (inner_related.equals(bf_right)){//两个RF相等
                                    //此时所有条件都达成，返回最终结果
                                    BinaryFormula result_right=new BinaryFormula(FormulaSign.EXIST,bf_left,tf_right.getRight());
                                    BinaryFormula result=new BinaryFormula(FormulaSign.ANY,tf_left,result_right);
                                    return result;
                                }else {return null;}
                            }else {return null;}
                        }else { return null; }
                    }else {return null;}
                }else {return null;}
            }
        }
        public String getRuleName(){
            return "AA";
        }
    },

    EE{//
        public Formula applyRule(ArrayList<Proof> f){
            // f.size() != 2 return null
            if (f.size()!=2){return null;}
            // f[0] not TripleFormula return null
            if (f.get(0).getConclusion() instanceof BinaryFormula){}else {
                return null;
            }
            // f[1] not BinaryFormula return null
            if (f.get(1).getConclusion() instanceof BinaryFormula){}else {
                return null;
            }
            //f[0]为tripleFormula
            BinaryFormula tf=(BinaryFormula) f.get(0).getConclusion();
            //判定f[1]中的两个formula是不是related的
            BinaryFormula bf=(BinaryFormula) f.get(1).getConclusion();

            if (bf.getLeft() instanceof BinaryFormula || bf.getRight() instanceof BinaryFormula){//确保bf中的两个element都是uf
                return null;
            }else {
                UnaryFormula bf_left=(UnaryFormula) bf.getLeft();
                UnaryFormula bf_right=(UnaryFormula) bf.getRight();
                //例子中的情况都是（q，qR）不确定存不存在（qR，q）的情况。目前只进行（q，qR）的情况判断，日后有需要再添加
                if (bf.getSign()==FormulaSign.ANY){
                    //条件满足，开始hasRelation的判断
                    if (bf_left.hasRelationWith(bf_right)){//binaryFormula方面所有条件满足，开始进行TripleFormula的条件判断
                        if (tf.getSign()==FormulaSign.EXIST && tf.getRight() instanceof BinaryFormula){
                            if(tf.getLeft() instanceof BinaryFormula || tf.getRight() instanceof UnaryFormula){//新增，确保tf的left必定为uf,right必为bf
                                return null;
                            }
                            UnaryFormula tf_left=(UnaryFormula) tf.getLeft();
                            BinaryFormula tf_right=(BinaryFormula) tf.getRight();
                            if (tf_right.getLeft() instanceof UnaryFormula){}else {return null;}//确保tf.right.left(此处为q)，必须是uf
                            UnaryFormula inner=(UnaryFormula) tf_right.getLeft();//此时为q，是uf类型
                            if (tf_right.getSign()==FormulaSign.EXIST){//不存在内部的relation formula
                                //判断tf中的bf的左侧第一个formula是否和外部bf的左侧第一个formula相等
                                if (inner.equals(bf_left)){
                                    //所有条件成立，返回最终结果
                                    BinaryFormula result_right=new BinaryFormula(FormulaSign.EXIST,bf_right,tf_right.getRight());
                                    BinaryFormula result=new BinaryFormula(FormulaSign.EXIST,tf_left,result_right);
                                    return result;
                                }else {return null;}
                            }else {return null;}
                        }else { return null; }
                    }else {return null;}
                }else {//bf_left属于RF，第二种情况，现在默认不存在这种情况，返回null。日后可以调整
                    //反正就是其他不合格的情况
                    return null;
                }
            }
        }
        public String getRuleName(){
            return "EE";
        }
    },

    AE{//
        public Formula applyRule(ArrayList<Proof> f){
            // f.size() != 2 return null
            if (f.size()!=2){return null;}
            // f[0] not TripleFormula return null
            if (f.get(0).getConclusion() instanceof BinaryFormula){}else {
                return null;
            }
            // f[1] not BinaryFormula return null
            if (f.get(1).getConclusion() instanceof BinaryFormula){}else {
                return null;
            }
            //f[0]为tripleFormula
            BinaryFormula tf=(BinaryFormula) f.get(0).getConclusion();
            //判定f[1]中的两个formula是不是related的
            BinaryFormula bf=(BinaryFormula) f.get(1).getConclusion();

            if (bf.getLeft() instanceof BinaryFormula || bf.getRight() instanceof BinaryFormula){//避免tf
                return null;
            }else {
                UnaryFormula bf_left=(UnaryFormula) bf.getLeft();
                UnaryFormula bf_right=(UnaryFormula) bf.getRight();
                //例子中的情况都是（q，qR）不确定存不存在（qR，q）的情况。目前只进行（q，qR）的情况判断，日后有需要再添加
                if (bf.getSign()==FormulaSign.ANY){
                    //条件满足，开始hasRelation的判断
                    if (bf_left.hasRelationWith(bf_right)){//binaryFormula方面所有条件满足，开始进行TripleFormula的条件判断
                        if (tf.getSign()==FormulaSign.ANY && tf.getRight() instanceof BinaryFormula){
                            if(tf.getLeft() instanceof BinaryFormula || tf.getRight() instanceof UnaryFormula){//新增，确保tf的left必定为uf,right必为bf
                                return null;
                            }
                            UnaryFormula tf_left=(UnaryFormula) tf.getLeft();
                            BinaryFormula tf_right=(BinaryFormula) tf.getRight();
                            if (tf_right.getLeft() instanceof UnaryFormula){}else {return null;}//确保tf.right.left(此处为q)，必须是uf
                            UnaryFormula inner=(UnaryFormula) tf_right.getLeft();
                            if (tf_right.getSign()==FormulaSign.EXIST){//不存在内部的relation formula
                                //判断tf中的bf的左侧第一个formula是否和外部bf的左侧第一个formula相等
                                if (inner.equals(bf_left)){
                                    //所有条件成立，返回最终结果
                                    BinaryFormula result_right=new BinaryFormula(FormulaSign.EXIST,bf_right,tf_right.getRight());
                                    BinaryFormula result=new BinaryFormula(FormulaSign.ANY,tf_left,result_right);
                                    return result;
                                }else {return null;}
                            }else {return null;}
                        }else {return null; }
                    }else {return null;}
                }else {//bf_left属于RF，第二种情况，现在默认不存在这种情况，返回null。日后可以调整
                    //反正就是其他不合格的情况
                    return null;
                }
            }
        }
        public String getRuleName(){
            return "AE";
        }
        },

    II{
        public Formula applyRule(ArrayList<Proof> f){//{EXIST(p,EXIST(q,t))}II -> EXIST(q,q)
            // f.size() != 1 return null
            if (f.size()!=1){return null;}
            // f[0] not BinaryFormula return null
            if (f.get(0).getConclusion() instanceof BinaryFormula){
                BinaryFormula tf=(BinaryFormula) f.get(0).getConclusion();

                if (tf.getLeft() instanceof UnaryFormula){}else {return null;}//tf.left必须为uf
                if (tf.getSign()==FormulaSign.EXIST){//判断整体（tf）的符号
                    if (tf.getRight() instanceof UnaryFormula){//避免uf存在的情况
                        return null;
                    }else {
                        BinaryFormula bf=(BinaryFormula) tf.getRight();
                        if (bf.getSign()==FormulaSign.EXIST){//判断tf内部，bf的符号
                            if (bf.getLeft() instanceof UnaryFormula){}else {return null;}//bf.left必须为uf
                            Formula bf_left=bf.getLeft();
                            BinaryFormula result=new BinaryFormula(FormulaSign.EXIST,bf_left,bf_left);
                            return result;
                        } else {return null;}
                    }
                }else {return null;}
            }else {
                return null;
            }
        }
        public String getRuleName(){
            return "II";
        }
    };


    public abstract Formula applyRule(ArrayList<Proof> f);
    public abstract String getRuleName();




}
